Nuprl Lemma : sublist_transitivity
11,40
postcript
pdf
T
:Type,
L1
,
L2
,
L3
:(
T
List). sublist(
T
;
L1
;
L2
)
sublist(
T
;
L2
;
L3
)
sublist(
T
;
L1
;
L3
)
latex
Definitions
t
T
,
compose(
f
;
g
)
,
suptype(
S
;
T
)
,
subtype(
S
;
T
)
,
x
:
A
.
B
(
x
)
,
,
int_seg(
i
;
j
)
,
P
Q
Lemmas
int
seg
wf
,
non
neg
length
,
length
wf1
,
compose
increasing
origin
T:Type, L1,L2,L3:(T List). sublist(T; L1; L2) 
sublist(T; L2; L3) sublist(T; L1; L3) T:Type, L1,L2,L3:(T List). sublist(T; L1; L2) sublist(T; L2; L3) sublist(T; L1; L3) 
Tx:A. B(x)
Q